Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

Q is empty.


QTRS
  ↳ Overlay + Local Confluence

Q restricted rewrite system:
The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

Q is empty.

The TRS is overlay and locally confluent. By [15] we can switch to innermost.

↳ QTRS
  ↳ Overlay + Local Confluence
QTRS
      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)


Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(rm, n)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(app'(filter2, app'(f, x)), f), x)
APP'(app'(eq, app'(s, x)), app'(s, y)) → APP'(app'(eq, x), y)
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(app'(add, app'(f, x)), app'(app'(map, f), xs))
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(app, app'(app'(rm, n), x)), y)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(app'(add, n), y)
APP'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, m), x))
APP'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(add, n), x)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(if_rm, app'(app'(eq, n), m)), n)
APP'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → APP'(rm, n)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(rm, n), x)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(min, app'(app'(add, n), x))
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(filter2, app'(f, x)), f)
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(le, n)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(eq, n)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(filter, f)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(minsort, app'(app'(app, app'(app'(rm, n), x)), y))
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(app'(add, m), app'(app'(rm, n), x))
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(filter2, app'(f, x))
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app'(add, n), app'(app'(app, x), y))
APP'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x))))
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(add, app'(f, x))
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app, app'(app'(rm, n), x))
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(app'(map, f), xs)
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(filter, f)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(add, x)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(minsort, x)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(filter, f), xs)
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app'(app, x), y)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(app'(minsort, x), app'(app'(add, n), y))
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(if_rm, app'(app'(eq, n), m))
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
APP'(app'(eq, app'(s, x)), app'(s, y)) → APP'(eq, x)
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app, x)
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(rm, n)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(if_min, app'(app'(le, n), m))
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(add, x), app'(app'(filter, f), xs))
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(eq, n)
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(app'(filter, f), xs)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(eq, n), app'(min, app'(app'(add, n), x)))
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(le, n), m)
APP'(app'(le, app'(s, x)), app'(s, y)) → APP'(app'(le, x), y)
APP'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, n), x))
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x))
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
APP'(app'(le, app'(s, x)), app'(s, y)) → APP'(le, x)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(eq, n), m)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
QDP
          ↳ EdgeDeletionProof

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(rm, n)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(app'(filter2, app'(f, x)), f), x)
APP'(app'(eq, app'(s, x)), app'(s, y)) → APP'(app'(eq, x), y)
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(app'(add, app'(f, x)), app'(app'(map, f), xs))
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(app, app'(app'(rm, n), x)), y)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(app'(add, n), y)
APP'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, m), x))
APP'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(add, n), x)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(if_rm, app'(app'(eq, n), m)), n)
APP'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → APP'(rm, n)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(rm, n), x)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(min, app'(app'(add, n), x))
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(filter2, app'(f, x)), f)
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(le, n)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(eq, n)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(filter, f)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(minsort, app'(app'(app, app'(app'(rm, n), x)), y))
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(app'(add, m), app'(app'(rm, n), x))
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(filter2, app'(f, x))
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app'(add, n), app'(app'(app, x), y))
APP'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x))))
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(add, app'(f, x))
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app, app'(app'(rm, n), x))
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(app'(map, f), xs)
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(filter, f)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(add, x)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(minsort, x)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(filter, f), xs)
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app'(app, x), y)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(app'(minsort, x), app'(app'(add, n), y))
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(if_rm, app'(app'(eq, n), m))
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
APP'(app'(eq, app'(s, x)), app'(s, y)) → APP'(eq, x)
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app, x)
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(rm, n)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(if_min, app'(app'(le, n), m))
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(add, x), app'(app'(filter, f), xs))
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(eq, n)
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(app'(filter, f), xs)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(eq, n), app'(min, app'(app'(add, n), x)))
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(le, n), m)
APP'(app'(le, app'(s, x)), app'(s, y)) → APP'(app'(le, x), y)
APP'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, n), x))
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x))
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
APP'(app'(le, app'(s, x)), app'(s, y)) → APP'(le, x)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(eq, n), m)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
We deleted some edges using various graph approximations

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ EdgeDeletionProof
QDP
              ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(rm, n)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(app'(filter2, app'(f, x)), f), x)
APP'(app'(eq, app'(s, x)), app'(s, y)) → APP'(app'(eq, x), y)
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(app'(add, app'(f, x)), app'(app'(map, f), xs))
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(app, app'(app'(rm, n), x)), y)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(app'(add, n), y)
APP'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, m), x))
APP'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(add, n), x)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(if_rm, app'(app'(eq, n), m)), n)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(rm, n), x)
APP'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → APP'(rm, n)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(min, app'(app'(add, n), x))
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(filter2, app'(f, x)), f)
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(le, n)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(eq, n)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(filter, f)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(minsort, app'(app'(app, app'(app'(rm, n), x)), y))
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(app'(add, m), app'(app'(rm, n), x))
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(filter2, app'(f, x))
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app'(add, n), app'(app'(app, x), y))
APP'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x))))
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(add, app'(f, x))
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app, app'(app'(rm, n), x))
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(app'(map, f), xs)
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(filter, f)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(add, x)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(minsort, x)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(filter, f), xs)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(app'(minsort, x), app'(app'(add, n), y))
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app'(app, x), y)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(if_rm, app'(app'(eq, n), m))
APP'(app'(eq, app'(s, x)), app'(s, y)) → APP'(eq, x)
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app, x)
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(rm, n)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(if_min, app'(app'(le, n), m))
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(eq, n)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(add, x), app'(app'(filter, f), xs))
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(eq, n), app'(min, app'(app'(add, n), x)))
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(app'(filter, f), xs)
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(le, n), m)
APP'(app'(le, app'(s, x)), app'(s, y)) → APP'(app'(le, x), y)
APP'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, n), x))
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x))
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil)
APP'(app'(le, app'(s, x)), app'(s, y)) → APP'(le, x)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(eq, n), m)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 7 SCCs with 37 less nodes.

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ EdgeDeletionProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
QDP
                    ↳ QDPOrderProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app'(app, x), y)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13]. Here, we combined the reduction pair processor with the A-transformation [14] which results in the following intermediate Q-DP Problem.
Q DP problem:
The TRS P consists of the following rules:

APP(add(n, x), y) → APP(x, y)

R is empty.
The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
map(x0, nil)
map(x0, add(x1, x2))
filter(x0, nil)
filter(x0, add(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.


The following pairs can be oriented strictly and are deleted.


APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app'(app, x), y)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
APP(x1, x2)  =  APP(x1)
add(x1, x2)  =  add(x1, x2)

Lexicographic path order with status [19].
Quasi-Precedence:
add2 > APP1

Status:
APP1: [1]
add2: [1,2]


The following usable rules [14] were oriented: none



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ EdgeDeletionProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                    ↳ QDPOrderProof
QDP
                        ↳ PisEmptyProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ EdgeDeletionProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
QDP
                    ↳ QDPOrderProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(le, app'(s, x)), app'(s, y)) → APP'(app'(le, x), y)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13]. Here, we combined the reduction pair processor with the A-transformation [14] which results in the following intermediate Q-DP Problem.
Q DP problem:
The TRS P consists of the following rules:

LE(s(x), s(y)) → LE(x, y)

R is empty.
The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
map(x0, nil)
map(x0, add(x1, x2))
filter(x0, nil)
filter(x0, add(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.


The following pairs can be oriented strictly and are deleted.


APP'(app'(le, app'(s, x)), app'(s, y)) → APP'(app'(le, x), y)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
LE(x1, x2)  =  LE(x2)
s(x1)  =  s(x1)

Lexicographic path order with status [19].
Quasi-Precedence:
s1 > LE1

Status:
LE1: [1]
s1: [1]


The following usable rules [14] were oriented: none



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ EdgeDeletionProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                    ↳ QDPOrderProof
QDP
                        ↳ PisEmptyProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ EdgeDeletionProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ QDPOrderProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, n), x))
APP'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, m), x))
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13]. Here, we combined the reduction pair processor with the A-transformation [14] which results in the following intermediate Q-DP Problem.
Q DP problem:
The TRS P consists of the following rules:

MIN(add(n, add(m, x))) → IF_MIN(le(n, m), add(n, add(m, x)))
IF_MIN(false, add(n, add(m, x))) → MIN(add(m, x))
IF_MIN(true, add(n, add(m, x))) → MIN(add(n, x))

The TRS R consists of the following rules:

le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
map(x0, nil)
map(x0, add(x1, x2))
filter(x0, nil)
filter(x0, add(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.


The following pairs can be oriented strictly and are deleted.


APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
The remaining pairs can at least be oriented weakly.

APP'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, n), x))
APP'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, m), x))
Used ordering: Combined order from the following AFS and order.
MIN(x1)  =  MIN(x1)
add(x1, x2)  =  add(x2)
IF_MIN(x1, x2)  =  x2
le(x1, x2)  =  le(x1, x2)
false  =  false
true  =  true
s(x1)  =  x1
0  =  0

Lexicographic path order with status [19].
Quasi-Precedence:
le2 > [MIN1, add1]
false > [MIN1, add1]
true > [MIN1, add1]
0 > [MIN1, add1]

Status:
MIN1: [1]
true: multiset
false: multiset
0: multiset
le2: [2,1]
add1: [1]


The following usable rules [14] were oriented: none



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ EdgeDeletionProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ QDPOrderProof
QDP
                        ↳ DependencyGraphProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, n), x))
APP'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, m), x))

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 0 SCCs with 2 less nodes.

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ EdgeDeletionProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ QDPOrderProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(eq, app'(s, x)), app'(s, y)) → APP'(app'(eq, x), y)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13]. Here, we combined the reduction pair processor with the A-transformation [14] which results in the following intermediate Q-DP Problem.
Q DP problem:
The TRS P consists of the following rules:

EQ(s(x), s(y)) → EQ(x, y)

R is empty.
The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
map(x0, nil)
map(x0, add(x1, x2))
filter(x0, nil)
filter(x0, add(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.


The following pairs can be oriented strictly and are deleted.


APP'(app'(eq, app'(s, x)), app'(s, y)) → APP'(app'(eq, x), y)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
EQ(x1, x2)  =  EQ(x2)
s(x1)  =  s(x1)

Lexicographic path order with status [19].
Quasi-Precedence:
s1 > EQ1

Status:
EQ1: [1]
s1: [1]


The following usable rules [14] were oriented: none



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ EdgeDeletionProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ QDPOrderProof
QDP
                        ↳ PisEmptyProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ EdgeDeletionProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ QDPOrderProof
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13]. Here, we combined the reduction pair processor with the A-transformation [14] which results in the following intermediate Q-DP Problem.
Q DP problem:
The TRS P consists of the following rules:

RM(n, add(m, x)) → IF_RM(eq(n, m), n, add(m, x))
IF_RM(true, n, add(m, x)) → RM(n, x)
IF_RM(false, n, add(m, x)) → RM(n, x)

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
map(x0, nil)
map(x0, add(x1, x2))
filter(x0, nil)
filter(x0, add(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.


The following pairs can be oriented strictly and are deleted.


APP'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)
The remaining pairs can at least be oriented weakly.

APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
Used ordering: Combined order from the following AFS and order.
RM(x1, x2)  =  RM(x1, x2)
add(x1, x2)  =  add(x1, x2)
IF_RM(x1, x2, x3)  =  IF_RM(x2, x3)
eq(x1, x2)  =  x1
true  =  true
false  =  false
0  =  0
s(x1)  =  s

Lexicographic path order with status [19].
Quasi-Precedence:
0 > true
s > false > [RM2, IFRM2] > add2

Status:
true: multiset
false: multiset
add2: [1,2]
0: multiset
s: []
RM2: [1,2]
IFRM2: [1,2]


The following usable rules [14] were oriented: none



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ EdgeDeletionProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ QDPOrderProof
QDP
                        ↳ DependencyGraphProof
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 0 SCCs with 1 less node.

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ EdgeDeletionProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(app'(minsort, x), app'(app'(add, n), y))
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ EdgeDeletionProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(app'(map, f), xs)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(filter, f), xs)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(app'(filter, f), xs)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(app'(map, f), xs)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
The remaining pairs can at least be oriented weakly.

APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(filter, f), xs)
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(app'(filter, f), xs)
Used ordering: Combined order from the following AFS and order.
APP'(x1, x2)  =  APP'(x2)
app'(x1, x2)  =  app'(x1, x2)
map  =  map
add  =  add
filter2  =  filter2
true  =  true
filter  =  filter
false  =  false
if_minsort  =  if_minsort
minsort  =  minsort
eq  =  eq
min  =  min
if_rm  =  if_rm
rm  =  rm
app  =  app
s  =  s
nil  =  nil
0  =  0
le  =  le
if_min  =  if_min

Lexicographic path order with status [19].
Quasi-Precedence:
[APP'1, filter2] > [map, add, true, nil, le] > filter > [app'2, app] > [eq, rm, s]
[APP'1, filter2] > [map, add, true, nil, le] > false > [app'2, app] > [eq, rm, s]
[APP'1, filter2] > [map, add, true, nil, le] > ifminsort > minsort > min > [app'2, app] > [eq, rm, s]
[APP'1, filter2] > [map, add, true, nil, le] > ifrm > [app'2, app] > [eq, rm, s]
[APP'1, filter2] > [map, add, true, nil, le] > ifmin > min > [app'2, app] > [eq, rm, s]
0 > [eq, rm, s]

Status:
app'2: [2,1]
map: multiset
eq: multiset
APP'1: [1]
min: multiset
app: multiset
0: multiset
rm: multiset
s: multiset
nil: multiset
add: multiset
ifmin: multiset
true: multiset
filter: multiset
ifrm: multiset
ifminsort: multiset
false: multiset
le: multiset
filter2: multiset
minsort: multiset


The following usable rules [14] were oriented: none



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ EdgeDeletionProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ QDPOrderProof
QDP
                        ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(filter, f), xs)
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(app'(filter, f), xs)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 0 SCCs with 2 less nodes.